
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">

<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<title>Module ErgoSpec.Common.Utils.Ast</title>
<meta name="description" content="Documentation of Coq module ErgoSpec.Common.Utils.Ast" />
<link href="coq2html.css" rel="stylesheet" type="text/css" />
<script type="text/javascript" src="coq2html.js"> </script>
</head>

<body onload="hideAll('proofscript')">
<h1 class="title">Module ErgoSpec.Common.Utils.Ast</h1>
<div class="coq">
<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html">String</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html">ErgoSpec.Backend.ErgoBackend</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html">ErgoSpec.Common.Utils.Names</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html">ErgoSpec.Common.Utils.Provenance</a></span>.<br/>
<br/>
<span class="kwd">Section</span> <span class="id"><a name="Ast">Ast</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Section</span> <span class="id"><a name="Ast.Imports">Imports</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Section</span> <span class="id"><a name="Ast.Imports.Defn">Defn</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Context</span> {<span class="id">A</span>:<span class="kwd">Set</span>}. <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Context</span> {<span class="id">N</span>:<span class="kwd">Set</span>}. <br/>
&nbsp;&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Inductive</span> <span class="id"><a name="import_decl">import_decl</a></span> : <span class="kwd">Set</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a name="ImportAll">ImportAll</a></span> : <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#Ast.Imports.Defn.A">A</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#namespace_name">namespace_name</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#import_decl">import_decl</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a name="ImportSelf">ImportSelf</a></span> : <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#Ast.Imports.Defn.A">A</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#namespace_name">namespace_name</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#import_decl">import_decl</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a name="ImportName">ImportName</a></span> : <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#Ast.Imports.Defn.A">A</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#namespace_name">namespace_name</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#local_name">local_name</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#import_decl">import_decl</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="import_annot">import_annot</a></span> (<span class="id">i</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#import_decl">import_decl</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#i">i</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#ImportAll">ImportAll</a></span> <span class="id">a</span> <span class="id">_</span> =&gt; <span class="id">a</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#ImportSelf">ImportSelf</a></span> <span class="id">a</span> <span class="id">_</span> =&gt; <span class="id">a</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#ImportName">ImportName</a></span> <span class="id">a</span> <span class="id">_</span> <span class="id">_</span> =&gt; <span class="id">a</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="extends">extends</a></span> : <span class="kwd">Set</span> := <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#Ast.Imports.Defn.N">N</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#Ast.Imports.Defn">Defn</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="limport_decl">limport_decl</a></span> : <span class="kwd">Set</span> := @<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#import_decl">import_decl</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#provenance">provenance</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="rextends">rextends</a></span> : <span class="kwd">Set</span> := @<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#extends">extends</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#relative_name">relative_name</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="aextends">aextends</a></span> : <span class="kwd">Set</span> := @<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#extends">extends</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#absolute_name">absolute_name</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#Ast.Imports">Imports</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Section</span> <span class="id"><a name="Ast.Abstract">Abstract</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="is_abstract">is_abstract</a></span> : <span class="kwd">Set</span> := <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#bool">bool</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<br/>
&nbsp;&nbsp;<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#Ast.Abstract">Abstract</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Section</span> <span class="id"><a name="Ast.Patterns">Patterns</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Section</span> <span class="id"><a name="Ast.Patterns.Defn">Defn</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Local</span> <span class="kwd">Open</span> <span class="kwd">Scope</span> <span class="id">string</span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Context</span> {<span class="id">A</span>:<span class="kwd">Set</span>}. <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Context</span> {<span class="id">N</span>:<span class="kwd">Set</span>}. <br/>
&nbsp;&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="type_annotation">type_annotation</a></span> : <span class="kwd">Set</span> := <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#Ast.Patterns.Defn.N">N</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Inductive</span> <span class="id"><a name="ergo_pattern">ergo_pattern</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a name="CaseData">CaseData</a></span> : <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#Ast.Patterns.Defn.A">A</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoData.data">ErgoData.data</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#ergo_pattern">ergo_pattern</a></span>                  <span class="docright">(* match against value  *)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a name="CaseWildcard">CaseWildcard</a></span> : <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#Ast.Patterns.Defn.A">A</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#type_annotation">type_annotation</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#ergo_pattern">ergo_pattern</a></span>            <span class="docright">(* match anything  *)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a name="CaseLet">CaseLet</a></span> : <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#Ast.Patterns.Defn.A">A</a></span> -&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#type_annotation">type_annotation</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#ergo_pattern">ergo_pattern</a></span>       <span class="docright">(* match against type  *)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a name="CaseLetOption">CaseLetOption</a></span> : <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#Ast.Patterns.Defn.A">A</a></span> -&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#type_annotation">type_annotation</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#ergo_pattern">ergo_pattern</a></span> <span class="docright">(* match against type  *)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#Ast.Patterns.Defn">Defn</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="rergo_pattern">rergo_pattern</a></span> {<span class="id">A</span>} := @<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#ergo_pattern">ergo_pattern</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#A">A</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#relative_name">relative_name</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="aergo_pattern">aergo_pattern</a></span> {<span class="id">A</span>} := @<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#ergo_pattern">ergo_pattern</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#A">A</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#absolute_name">absolute_name</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="lrergo_pattern">lrergo_pattern</a></span> := @<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#ergo_pattern">ergo_pattern</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#provenance">provenance</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#relative_name">relative_name</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="laergo_pattern">laergo_pattern</a></span> := @<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#ergo_pattern">ergo_pattern</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#provenance">provenance</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#absolute_name">absolute_name</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#Ast.Patterns">Patterns</a></span>.<br/>
&nbsp;&nbsp;<br/>
<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#Ast">Ast</a></span>.<br/>

</div>
<div class="footer"><hr/>Generated by <a href="https://github.com/xavierleroy/coq2html/">coq2html</div>
</body>
</html>
